COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "memo.pub[let,jmc]" source
C00016 00003
C00017 ENDMK
C⊗;
.require "memo.pub[let,jmc]" source;
.double space
.at "qF" ⊂"%AF%*"⊃
.cb AN INDUCTION PRINCIPLE FOR CYCLIC LIST STRUCTURES AND GRAPHS

.cb "John McCarthy, Stanford University"


	The subject of this note is an axiom schema for cyclic
list structures.  It allows computer-checkable first order logic
proofs of facts about programs that traverse such structures.
Since cyclic list structures do not form an inductively defined set, some
innovation was needed.  There is also a transfinite version.

	Cyclic or re-entrant list structures are second class citizens
in most LISPs.  They can be created using ⊗rplaca and ⊗rplacd, but most
LISPs can't print them, the standard theories for proving assertions
about programs don't apply to them,
 and special programs have to be written
to compute with them.  The main characteristic of such programs
is that in order to avoid infinite recursions,
they must carry along a list of nodes already visited that
is compared with the current node.  This provides the essential
clue to finding a new induction principle that applies to them.

	From another point of view we are talking about finite
binary directed graphs, which we shall call fbd graphs
for short.  Looked at set-theoretically, an fbd graph
consists of a finite set ⊗A, a unary predicate ⊗atom, and
two maps ⊗car and ⊗cdr from the non-atoms into ⊗A. 

	A full theory of programs on fbd graphs would include
operations that produce and change graphs.  We don't have that yet, and
the formalism of (Morris and Schwarz 1980) which includes such operations
may not be easy to axiomatize.
However, we do have an axiom schema in first order logic that
permits computer checkable first order logic proofs of
facts about programs that traverse fbd graphs
using operations ⊗car, ⊗cdr, equality and the test for ⊗atom on the graph
and ordinary LISP operations on lists of nodes and other entities.

	We will use ⊗x for a variable ranging over nodes in fbd graphs
and ⊗u, ⊗v and ⊗w for variables ranging over lists whose elements
may be such nodes but which terminate in qnil just like the usual LISP
lists.
We also use the notation of (McCarthy and Talcott 1980) of qa for ⊗car, qd
for ⊗cdr, infixed . for ⊗cons and qat for ⊗atom. 

	Unlike trees, fbd graphs are not inductively defined structures.
Nevertheless, there is an axiom schema that we will call
the graph induction schema, namely

!!a4:	%2∀x u.(qat x ∨ x ε u ∨ qF(qa x, x.u) ∧ qF(qd x, x.u) ⊃ qF(x,u))
⊃ ∀x u.qF(x,u)%1.

The variable ⊗u in the schema is a list of nodes for which nothing has
to be proved, and the finiteness of the graph insures that as we go
down in the graph we eventually hit either atoms or nodes already examined.
It may help understanding to note that the schema corresponds to the
termination of the LISP-type predicate ⊗isfbdg (for "is finite binary
directed graph")
defined by

	%2isfbdg x ← isfbdg1[x,qnil]%1,

	%2isfbdg1[x,u] ←
  qat x ∨ x ε u ∨ isfbdg1[qa x, x.u] ∧ isfbdg1[qd x, x.u]%1.

The statement that ⊗isfbdg always terminates corresponds to the local
finiteness of the graph.  Starting from any vertex, only a finite number
can be reached.

	This can be compared with the induction schema for S-expressions,
i.e. finite binary trees, namely

!!a5:	%2∀x.(qat x ∨ qF(qa x) ∧ qF(qd x) ⊃ qF(x)) ⊃ ∀x.qF(x)%1.

The Peano axiom schema for natural numbers
 may be written in a corresponding "down going" form,
namely

!!a6:	%2∀n.(n = 0 ∨ qF(n%5-%2) ⊃ qF(n)) ⊃ ∀n.qF(n)%1

These too correspond to the termination of certain recursively
defined predicates, namely

!!a2:	%2issexp x ← qat x ∨ issexp qa x ∧ issexp qd x%1

for S-expressions, and

!!a3:	%2isnatnum n ← n=0 ∨ isnatnum n%5-%1.

for natural numbers.

	The need for the extra variable ⊗u in graph induction comes from
the fact that graphs are not an inductively defined
set in any obvious sense.  The analogy with relative concepts in
topology, e.g. relative homology groups, may be suggestive.

	Graph induction can be informally justified by regarding
the rank of an %2<x,_u>%1 pair as the number of nodes in the
graph not included in ⊗u.  If %2∀x.qF(x,_u)%1 is false, then there
is a counter example of least rank, say %2<x0,_u0>%1.  If %2x0_ε_u0%1
or ⊗x0 is atomic, the premisses of the induction are violated.  Otherwise,
⊗x0 is neither atomic nor in ⊗u0.  If %2qF(qa_x0,_x0.u0)_∧_qF(qd_x0,_x0.u0)%1
is true, the third premiss of the induction is violated.  But then
either %2qF(qa_x0,_x0.u0)%1 or %2qF(qd_x0,_x0.u0)%1 would constitute
a counter-example of lower rank.  This concludes the proof.

	We emphasize that the variable ⊗x ranges over the nodes of
a single connected graph.  However, if the specific properties of the
graph aren't used, the result is valid for all nodes of all fbdgs.


%3Example:%1

	We use the techniques of (Cartwright 1977) and
graph induction to prove total the function

!!a10:	%2nodes[x,u] ← qif x ε u qthen u qelse qif qat x qthen x.u
qelse nodes[qd x, nodes[qa x, u]]%1,

whose value is a list of nodes reachable from ⊗x that are not in
the list ⊗u. 

	The function ⊗nodes defined by the recursive program ({eq a10})
satisfies the functional equation

!!a11:	%2∀x u.(nodes[x,u] = qif x ε u qthen u qelse qif qat x qthen x.u
qelse nodes[qd x, nodes[qa x, u]])%1,

where = has replaced ←, and the domain has been extended by an undefined
element taken to be the value of a function when the computation
doesn't terminate.  Hence

	%2∀x u.islist_nodes[x,u]%1

is the assertion that for all nodes ⊗x and lists ⊗u the value of the
function is a list, i.e. not the undefined element.  This theory is
is explained in (Cartwright and McCarthy 1979) and in (McCarthy and
Talcott 1980).

	To make the induction work, we prove the more general statement

!!a8:	%2∀x u.(∀w. u ⊂ w ⊃ islist nodes[x,w] ∧ u ⊂ nodes[x,w])%1.

Here %2u_⊂_v%1
means that every element of the list ⊗u is a member of the list ⊗v, and
our proof uses obvious properties of ⊂ which can be proved by list
induction from a suitable recursive definition of %2u_⊂_v%1.

	We now take

!!a9:	%2qF(x,u) ≡ ∀w.(u ⊂ w ⊃ islist nodes[x,w] ∧ u ⊂ nodes[x,w])%1.

and prove %2qF(x,u)%1 assuming succesively %2x ε u%1, %2qat x%1 and
%2qF(qa_x,_u)%1_∧_%2qF(qa_x,_u)%1 as is required to use the schema ({eq a4}).

	The cases %2x ε u%1 and %2qat x%1 are absolutely straightforward.
%2qF(qa x, x.u)%1 takes the form 

	%2∀v.(x.u ⊂ v ⊃ islist nodes[qa x, v] ∧ x.u ⊂ nodes[qa x, v])%1,

and we specialize this by choosing %2v = x.w%1, getting

	%2islist nodes[qa x, x.w] ∧ x.u ⊂ nodes[qa x, x.w]%1.

%2qF(qd x, x.u)%1 takes the form

	%2∀v.(x.u ⊂ v ⊃ islist nodes[qd x, v] ∧ x.u ⊂ nodes[qd x, v]%1,

and we specialize it by choosing %2v = nodes[qa x, x.w]%1, getting eventually

	%2islist nodes[qd x, nodes[qa x, x.w]] ∧ u ⊂ nodes[qd x,
nodes[qa x, x.w]]%1,

which is all we need to complete the proof.


.if false then begin

cyclic.lsp[e80,jmc] has the actual functions

To show that a search defined with a narrower notion of successor
terminates whenever the original search terminates is a good problem.
.end
.skip 2
.bb Exercises:

.item←0
	Write and prove total programs as follows:

	#. A program that represents a graph as a list of three
element lists of atoms.  For each non-atomic node there is a
list consisting of this element followed by its ⊗car and its
⊗cdr.  On such lists one can define operations ⊗car1 and ⊗cdr1 and
prove the isomorphism between them and ⊗car and ⊗cdr on the
original graphs.  The fact that ⊗gensym() is not a function
in the mathematical sense has to be somehow finessed.

	#. Write and prove some facts about a program that searches
a graph for a vertex with a given property.

	#. Write a program that tests graphs for isomorphisms of
various kinds.
.skip 2
.bb References:

%3Cartwright, R.S. (1977)%1:
%2A Practical Formal Semantic Definition and Verification System
for Typed Lisp%1,
Ph.D. Thesis, Computer Science Department, Stanford University,
Stanford, California.

%3Cartwright, Robert and John McCarthy (1979)%1:
"Recursive Programs as Functions in a First Order Theory",
in %2Proceedings of the International Conference on Mathematical Studies of
Information Processing%1, Kyoto, Japan.

%3McCarthy, John and Carolyn Talcott (1980)%1: %2LISP - Programming and
Proving%1, course notes, Stanford University. (to be published as a book).

%3Morris, L. and J. Schwarz (1980)%1: "Computing Cyclic List Structures",
in %2Conference Record of the 1980 LISP Conference%1, The LISP Conference,
P.O. Box 487, Redwood Estates, CA 95044.

This version of CYCLIC[E80,JMC] pubbed on {date}.